$\forall$$A$:Type, $f$,$g$:fpf($A$; $a$.top), ${\it eq}$:EqDecider($A$), $x$:$A$.
\\[0ex]($x$ $\in$ fpf{-}domain(fpf{-}join(${\it eq}$; $f$; $g$))) $\Leftarrow\!\Rightarrow$ (($x$ $\in$ fpf{-}domain($f$)) $\vee$ ($x$ $\in$ fpf{-}domain($g$)))